es:ES, X:AbsInterface(Top), f:(E(X)E(X)). (x:E(X). f(x) c x)  (e:E(X). f**(e)  E(X)) 

latex

Definitions

(x  l), (e <loc e'), e loc e' , sender(e), suptype(S; T), S  T, e  X, f**(e), P  Q, (e < e'), e c e', first(e), pred(e), A, <a, b>, pred!(e;e'), , SWellFounded(R(x;y)), kind(e), loc(e), State(ds), State(ds), state@i, vartype(i;x), loc(e), f(x)?z, f  g, P  Q, P  Q, t.1, E, {x:A| B(x)} , let x,y = A in B(x;y), E(X), AbsInterface(A), strong-subtype(A;B), Top, P & Q, constant_function(f;A;B), b, , P  Q, r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), x,y. t(x;y), x. t(x), Knd, EState(T), f(a), EOrderAxioms(E; pred?; info), Id, IdLnk, left + right, Unit, EqDecider(T), Type, x:A  B(x), a:A fp B(a), ES, x:A. B(x), x:AB(x), t  T, s = t

Lemmas

subtype rel wf, event system wf, deq wf, unit wf, IdLnk wf, Id wf, EOrderAxioms wf, EState wf, Knd wf, kindcase wf, Msg wf, nat wf, rationals wf, val-axiom wf, cless wf, qle wf, bool wf, assert wf, constant function wf, top wf, member wf, es-E-interface wf, es-E wf, strongwellfounded wf, pred! wf, loc wf, not wf, es-causle wf, es-causl wf, strong-subtype-self, strong-subtype wf, strong-subtype-set3, es-fix wf, es-le-causle, subtype rel function, es-interface wf